PRISM
=====
Version: 4.5.dev
Date: Sat Mar 14 15:27:13 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -ii -heuristic speed -e 1e-6 -ddextraactionvars 100 -maxiters 1000000 consensus.4.prism consensus.props --property steps_min -const K=4
Parsing model file "consensus.4.prism"...
Type: MDP
Modules: process1 process2 process3 process4
Variables: counter pc1 coin1 pc2 coin2 pc3 coin3 pc4 coin4
Parsing properties file "consensus.props"...
5 properties:
(1) "c1": P>=1 [ F "finished" ]
(2) "c2": Pmin=? [ F "finished"&"all_coins_equal_1" ]
(3) "disagree": Pmax=? [ F "finished"&!"agree" ]
(4) "steps_max": R{"steps"}max=? [ F "finished" ]
(5) "steps_min": R{"steps"}min=? [ F "finished" ]
---------------------------------------------------------------------
Model checking: "steps_min": R{"steps"}min=? [ F "finished" ]
Model constants: K=4
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Warning: Switching to explicit engine to allow interval iteration on Rmin operator.
Building model...
Model constants: K=4
Computing reachable states... 43136 states
Reachable states exploration and model construction done in 0.668 secs.
Sorting reachable states list...
Time for model construction: 0.894 seconds.
Type: MDP
States: 43136 (1 initial)
Transitions: 144352
Choices: 115840
Max/avg: 4/2.69
Building reward structure...
Starting expected reachability (min)...
Starting Prob1 (max)...
Prob1 (max) took 57 iterations and 0.196 seconds.
target=64, inf=0, rest=43072
For Rmin, checking for zero-reward ECs...
Time for checking for zero-reward ECs: 0.058 seconds, no zero-reward ECs found, proceeding normally.
Computing upper bound(s) for Rmin using the Dijkstra Sweep for Monotone Pessimistic Initialization algorithm...
Calculating incoming choices relation for Markov decision process... done (0.042 seconds)
Time for computing upper bound(s) for Rmin using the DSI-MP algorithm: 0.39 seconds.
Upper bound for min expectation (Dijkstra Sweep MPI): 294914.0
Starting Prob1 (min)...
Prob1 (min) took 66 iterations and 0.185 seconds.
Relevant sub-MDP is contracting, proceed...
Starting interval iteration (min, with Power method)...
Iteration 1248: max relative diff=76.7538968888, 5.01 sec so far
Iteration 2511: max relative diff=8.81441439055, 10.01 sec so far
Iteration 3775: max relative diff=1.13648802001, 15.01 sec so far
Iteration 5046: max relative diff=0.146687358576, 20.02 sec so far
Iteration 6316: max relative diff=0.0189920162475, 25.02 sec so far
Iteration 7586: max relative diff=0.00245953934848, 30.02 sec so far
Iteration 8856: max relative diff=0.00031912507267, 35.02 sec so far
Iteration 10127: max relative diff=4.12756656092e-05, 40.03 sec so far
Iteration 11392: max relative diff=5.39036085568e-06, 45.03 sec so far
Max relative diff between upper and lower bound on convergence: 9.9779577472e-07
Interval iteration (min, with Power method) took 12440 iterations, 3589885440 multiplications and 49.191 seconds.
Maximum finite value in solution vector at end of interval iteration: 776.0003830222761
Expected reachability took 50.071 seconds.
Value in the initial state: 768.0003793450269
Time for model checking: 50.171 seconds.
Result: 768.0003793450269 (value in the initial state)
Overall running time: 51.665 seconds.
---------------------------------------------------------------------
Note: There were 2 warnings during computation.